$\forall$$P$:(ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$). es{-}real\{i:l\}(${\it es}$.$P$(${\it es}$)) $\in$ Type$_{\mbox{\scriptsize i''}}$